-----------------------------------------------------------------------------
--
-- Module      :  Data.Units.Types
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  eduard.sergeev@gmail.com
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level types and operations
--
-----------------------------------------------------------------------------

{-# LANGUAGE NoImplicitPrelude, TypeOperators, TypeFamilies,
FlexibleInstances, ScopedTypeVariables, UndecidableInstances #-}


module Data.Units.Types (

   ToCanonical,
   ToNumber,

   ToList,
   FromList,

   Convert,
   Unconvert,
            
   Force,
   Fo,

   U,

   (:*:),
   (:/:),

--   Remove,
--   Union,
--   Except,

   Multiply,
   Divide,
   SquareRoot,
   Power,

   EvenPowers,

) where

import Prelude (Show(show),Num((+)))
import Data.Eq
import Data.Char
import Data.Tuple
import Data.Function
import Data.Maybe
import Data.List

import Data.TypeLevel.Class
import Data.TypeLevel.Boolean
import Data.TypeLevel.Peano
--import Data.TypeLevel.Numbers



-- | Conversion
type family ToNumber u :: *
type instance ToNumber U = Zero

type family ToList u :: *
type instance ToList (a :/: b) = (ToList a) :/: (ToList b)
type instance ToList (a :*: b) = (ToList a) :*: b
type instance ToList U = U



type family FromList u :: *
type instance FromList (a :/: b) = (FromList a)  :/: (FromList b)
type instance FromList U = U

type family Convert u :: *
type instance Convert u = ToList u

type family Unconvert u :: *
type instance Unconvert u = FromList u


class Force v where
    type Fo v :: *
    force :: Fo v -> Fo v

instance Force v where
    type Fo v = v
    force _ = typeValue :: Fo v



-------------------
-- operators
-------------------

data a :*: b
data a :/: b

infixl 7 :*:
infixl 6 :/: 

-- Unit type (1, mzero)
data U
instance Show U where show _ = "1"


--------------------
-- Type List
--------------------

type Singleton a = U :*: a


-- | Inserts an element into the list in accordance to it's 'peano rank'
type family InsertBefore c e
type instance InsertBefore (t :*: h) e = InsertBefore' (ToNumber h :<=: ToNumber e) (t :*: h) e
type instance InsertBefore U e = (U :*: e)

type family InsertBefore' p c e
type instance InsertBefore' True l e = (l :*: e)
type instance InsertBefore' False (t :*: h) e = (InsertBefore t e) :*: h


-- | Union for lists
type family Union l r
type instance Union l (o t h) = Union (InsertBefore l h) t
type instance Union l U = l


-- | Type-level Maybe's Just
data Just a
-- | Type-level Maybe's Nothing
data Nothing


type family Remove c e :: *
type instance Remove (t :*: h) e = Remove' (ToNumber h :==: ToNumber e) (t :*: h) e
type instance Remove U e = (U,Just e)

type family Remove' p c e :: *
type instance Remove' True (t :*: h) e = (t,Nothing)
type instance Remove' False (t :*: h) e = Fs (Remove t e) h
type family Fs p h
type instance Fs (a,b) h = ((a :*: h) , b)


---
type family Except l r
type instance Except l (t :*: h) = Cs1 t (Remove l h)
type instance Except l U = (l,U)
type family Cs1 t r
type instance Cs1 t (l1,h1) = Cs2 (Except l1 t) h1
type family Cs2 p h
type instance Cs2 (l2,e2) h1 = (l2 , IB e2 h1)

type family IB a b
type instance IB l (Just h) = InsertBefore l h
type instance IB l Nothing = l


-----------------------
-- Num type operations
-----------------------
type family Mult a b

--type instance Mult (nl :/: dl) (nr :/: dr) = Div (Mult nl nr) (Mult dl dr)
type instance Mult (nl :/: dl) (nr :/: dr) = Comb2 (Except nl dr) (Except nr dl)


type instance Mult (t :*: h) (nr :/: dr) = Div (Mult (t :*: h) nr) dr 
type instance Mult (nl :/: dl) (t :*: h) = Mult (t :*: h) (nl :/: dl)
type instance Mult (tl :*: hl) (tr :*: hr) = Union (tl :*: hl) (tr :*: hr)
type instance Mult U (n :/: d) = (n :/: d)
type instance Mult U (n :*: d) = (n :*: d)
type instance Mult e U = e


---
type family Div n d
type instance Div (nl :/: dl) (nr :/: dr) = Div (Mult nl dr) (Mult dl nr)
type instance Div (nl :/: dl) (tr :*: hr) = Div nl (Mult dl (tr :*: hr))
type instance Div (tl :*: hl) (nr :/: dr) = Div (Mult (tl :*: hl) dr) nr
type instance Div (tl :*: hl) (tr :*: hr) = Comb (Except (tl :*: hl) (tr :*: hr))
type instance Div U (n :/: d) = (d :/: n)
type instance Div U (n :*: d) = (U :/: n :*: d)
type instance Div e U = e

type family Comb a
type instance Comb (U,U) = U
type instance Comb (U , (t :*: h)) = (U :/: t :*: h)
type instance Comb ((t :*: h) , U) = t :*: h
type instance Comb ((tl :*: hl) , (tr :*: hr)) = (tl :*: hl :/: tr :*: hr)

type family Comb2 a b
type instance Comb2 (la,lb) (ra,rb) = (Union la ra) :/: (Union lb rb)
--

type family Sqrt u
type instance Sqrt U = U
type instance Sqrt (n :/: d) = (Sqrt n) :/: (Sqrt d)
type instance Sqrt (t :*: u :*: u) = (Sqrt t) :*: u
---

type family Pow u p
type instance Pow u Zero = U
type instance Pow u (Succ n) = Mult u (Pow u n)  
--


type family Divide n d
type instance Divide n d = Unconvert (Div (Convert n) (Convert d))

type family Multiply a b
type instance Multiply a b = Unconvert (Mult (Convert a) (Convert b))

type family SquareRoot u
type instance SquareRoot u = Unconvert (Sqrt (Convert u))

type family Power u p
type instance Power u p = Unconvert (Pow (Convert u) p)


-- * Unit-related predicates
-- | All units in 'u' are of even powers ('m^2' , 'm^-4 s^6' etc.)
-- is used by "sqrt" function for its applicability check
class EvenPowers u
instance EvenPowers U
instance EvenPowers (u :*: u)
instance (EvenPowers t) => EvenPowers (t :*: u :*: u)
instance (EvenPowers n, EvenPowers d) => EvenPowers (n :/: d)



-- * "Show" and related

data Plus
data Minus

instance Show Plus where
    show _ = ""

instance Show Minus where
    show _ = "-"

data Canonical c
data Triple m s p

type family ToCanonical a :: *
type instance ToCanonical a = Chop (Signify (Normalize a))

type family Chop a :: *
type instance Chop (U :/: d) = U :/: (Chop d)
type instance Chop ((t :*: h) :/: d) = (Chop (t :*: h)) :/: (Chop d)
type instance Chop (t :*: h2 :*: h1) = (Chop (t :*: h2)) :*: h1
type instance Chop (U :*: h) = h
type instance Chop U = U

type family Signify a :: *
type instance Signify U = U
type instance Signify (t :*: h) = AddSign Plus (t :*: h)
type instance Signify (n :/: (h :*: (m2,p2) :*: (m1,p1))) = Union (AddSign Plus n) (AddSign Minus (h :*: (m2,p2) :*: (m1,p1)))
type instance Signify (n :/: (U :*: (m,p))) = (AddSign Plus n) :/:  (U :*: (Triple m Plus p))

type family Normalize a :: *
type instance Normalize U = U
type instance Normalize (t :*: h) = Aggregate t (h,One)
type instance Normalize (n :/: d) = (Normalize n) :/: (Normalize d)

type family AddSign s a :: *
type instance AddSign s U = U
type instance AddSign s (t :*: (m,p)) = AddSign s t :*: (Triple m s p)-- (m,s,p)

type family Aggregate h a :: *
type instance Aggregate U (m,p) = U :*: (m,p)
type instance Aggregate (t :*: h) (m,p) = Op (ToNumber h :==: ToNumber m) t h (m,p)

type family Op b t u a :: *
type instance Op True t u (u,p) = Aggregate t (u,Succ p)
type instance Op False t u1 u2p = (Aggregate t (u1,One)) :*: u2p 

type instance ToNumber (Triple m s p) = ToNumber m


instance (Show t, Show h) => Show (t :*: h) where
    show _ = show (typeValue :: t) ++ " " ++ show (typeValue :: h)

instance (Show n, Show d) => Show (n :/: d) where
    show _ = show (typeValue :: n) ++ "/" ++ show (typeValue :: d)

instance (Show m, Show s, Show p) => Show (Triple m s p) where
    show _ = show (typeValue :: m) ++ adjust ("^" ++ show (typeValue :: s) ++ show (typeValue :: p))
        where
          adjust "^1" = ""
          adjust s = s

{-
instance (Show m) => Show (Triple m Plus One) where
    show _ = show (typeValue :: m)

instance (Show m) => Show (Triple m Minus One) where
    show _ = show (typeValue :: m) ++ "^-1"

instance (Show m, Show s, Show (Succ (Succ p))) => Show (Triple m s (Succ (Succ p))) where
    show _ = show (typeValue :: m) ++ "^" ++ show (typeValue :: s) ++ show (typeValue :: Succ (Succ p))
-}
